| Definitions | t  T, State(ds), x:A  B(x),  x:A. B(x), S  T, State(ds), @i (with ds: ds action a:T precondition a is P s), es is an event system of D, ES, Type, {x:A| B(x)} ,  , suptype(S; T), @i Precondition for a:Outcome(p) is P:State(ds) ,  ,  x.A(x), P   Q,  x. t(x), Id, FinProbSpace, a:A fp B(a), D realizes es. P(es),  b, (initial state @ i)+t, (state after e)+t, PossibleWorld(D;w), FairFifo, World, D realizes2 es.P(es), locl(a), ES(the_w), es-kind-index(es;k;e), random(p;a;b), f(a), val(e), Outcome, s = t, valtype(e), A c B, kind(e), Knd, e@i. P(e), tt, IdDeq, eqof(d), s ~ t, Atom$n, x:A  B(x), hd(l), w-discrete-constraint(w), w-atom-constraint(w), w-machine-constraint(w), A  B, i  j , w-machine-independent(w;i;k;x), unsolvable M.pre(a,s),  A, M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), ma-random(M;T;v;i;a;n), M.pre(a,s), M.init(x,v),  , False, time(e), loc(e), t.2, t.1, isnull(a), <a, b>, E,  , es_info(es), {T}, SQType(T), loc(e), E, a(i;t), kind(a), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , act(e), es-V(es), tag(e), lnk(e), es-M(es), acttype(e), rcvtype(e), isrcv(e), True,  T, SqStable(P), act(k), left + right, isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), P  Q, z != f(x) P(a;z), let x,y,z = a in t(x;y;z), P  Q, P & Q, P Q, x dom(f), islocal(k), M.da(a), mk-ma, x : v, f(x)?z, (precondition a:Outcome(p) is P:State(ds) -> Bool), M.ds(x), M.bframe(k sends on l), M(i), M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), [], [car / cdr], f(x), valtype(i;a), w.TA, act(e), es_val(es), val(e), IdLnk, a declared in M, Void, act_locl{act_locl_compseq_tag_def:ObjectId}(a), ff, a = b, p  q,  x:A. B(x), es_init(es),  , (timed)state after e, e'e.P(e'), (state when e), Top, vartype(i;x), es_time(es), es-Trans(es), es-pred?(es), es_state_when(es;e), x when e, es-T(es), vartype(i;x), deq-member(eq;x;L), b, Unit, type List, (x l), product-deq(A;B;a;b), kind(e), Action(i), state_when(e),  , world-es-const, discrete(i;x), w-causl-time2, world-es-atom, world-es-val, w-machine(w;i), #$n, s(i;t).x, w.M, w.T, w-order-axioms, w-info(w;e), w-pred(w;e), NatDeq, time(e), state_when(e), read-state(s), a < b, e loc e' , n+m, (e < e'), (e <loc e'), loc(e), Dec(P), e < e', state_after(e), kind(e),  x:A.B(x), KindDeq, x,y. t(x;y), -n, n - m, r - s, r + s, x,y:A//B(x;y), r * s, i j < k, {i..j }, timedState(ds) |
| Lemmas | assert-eq-knd, subtype rel dep function, subtype rel function, read-state wf2, decidable ex int seg, decidable not, int seg wf, qmul over plus qrng, qmul one qrng, mon assoc q, qadd comm q, qadd ac 1 q, mon ident q, qmul wf, qadd-add, w-s wf, fpf-cap wf, qadd wf, qsub wf, int-rational, w-state-after, w-stutter, w-kind wf, decidable le, decidable assert, ge wf, nat properties, fpf-val-single1, fpf-single-dom, Kind-deq wf, loc wf, kind wf, w state after wf, cless wf, w-info wf, w-pred wf, decidable lt, w-cless-loc, le wf, rationals wf, int inc rationals, w-state-when, squash wf, true wf, w-a-not-null, w-time wf, w-E wf, w-loc wf, w-ekind wf, fpf-ap wf, not functionality wrt iff, assert-deq-member, l member wf, eqtt to assert, eqff to assert, assert of bnot, bnot wf, top wf, fpf-dom wf, fpf-trivial-subtype-top, deq-member wf, w-vartype wf, bor wf, eq id wf, bfalse wf, false wf, subtype rel self, subtype rel transitivity, iff transitivity, assert of bor, or functionality wrt iff, assert-eq-id, Knd sq, sq stable subtype rel, es-valtype wf, p-outcome wf, es-E wf, w-es wf, es-loc wf, Knd wf, es-kind wf, locl wf, w-loc-lemma, Id sq, w-kind-lemma, not wf, assert wf, w-isnull wf, pi1 wf, nat wf, w-a wf, pi2 wf, es-kind-index-w-knum, world wf, fair-fifo wf, possible-world wf, eqof eq btrue, id-deq wf, ma-state wf, fpf wf, finite-prob-space wf, Id wf, d-realizes2-implies-realizes, d-single-pre wf, pre-p wf, bool wf, decl-state wf, event system wf, d-es wf |